FSessionInvariants
R1341 Datatypes <> <> lib
R1367 Prelude <> <> lib
R1391 State <> <> lib
R1413 Events <> <> lib
R1436 Behavior <> <> lib
R1461 StepInvariants <> <> lib
R1492 Session <> <> lib
sec 1511 <> SESSION_INVARIANTS
var 1541 SESSION_INVARIANTS policy
R1550 Prelude <> Policy rec
def 1628 <> IsInvariant
R1804 Session <> mkStep constr
R1784 Session <> mkStep constr
R1761 Coq.Init.Logic "x <> y" not
R1764 Events <> terminate constr
R1734 Behavior <> Chi ind
R1716 Events <> Event ind
R1716 Events <> Event ind
R1694 Coq.Init.Datatypes <> option ind
R1701 Behavior <> Response ind
R1694 Coq.Init.Datatypes <> option ind
R1701 Behavior <> Response ind
R1682 State <> State rec
R1682 State <> State rec
R1643 Session <> Step rec
sec 1832 SESSION_INVARIANTS SOME_INVARIANTS
var 1861 SESSION_INVARIANTS.SOME_INVARIANTS s0
R1866 State <> State rec
var 1883 SESSION_INVARIANTS.SOME_INVARIANTS sid
R1889 Prelude <> SuiteID defax
var 2083 SESSION_INVARIANTS.SOME_INVARIANTS vr
R2088 Prelude <> VendorRepository rec
var 2116 SESSION_INVARIANTS.SOME_INVARIANTS cert
R2123 Prelude <> Certificate rec
var 2149 SESSION_INVARIANTS.SOME_INVARIANTS HValid
R2158 State <> Valid def
prf 2255 <> psinv_valid
R2339 Datatypes <> all ind
R2356 State <> Valid def
R2370 Session <> step_s proj
R2299 Session <> PartialSession ind
R2283 Datatypes <> seq ind
R2287 Session <> Step rec
R2523 Datatypes <> all_snoc constr
R2523 Datatypes <> all_snoc constr
R2543 Datatypes <> all_nil constr
R2543 Datatypes <> all_nil constr
R2653 Events <> start constr
R2631 StepInvariants <> inv_valid thm
R2653 Events <> start constr
R2631 StepInvariants <> inv_valid thm
R2716 Datatypes <> all_snoc constr
R2716 Datatypes <> all_snoc constr
R2968 Session <> step_s proj
R2952 StepInvariants <> inv_valid thm
R2968 Session <> step_s proj
R2952 StepInvariants <> inv_valid thm
prf 3081 <> sinv_valid
R3157 Datatypes <> all ind
R3171 State <> Valid def
R3185 Session <> step_s proj
R3124 Session <> Session ind
R3108 Datatypes <> seq ind
R3112 Session <> Step rec
R3415 Datatypes <> all_snoc constr
R3415 Datatypes <> all_snoc constr
R3476 SessionInvariants <> psinv_valid thm
R3476 SessionInvariants <> psinv_valid thm
R3617 Datatypes <> all ind
R3660 Datatypes "l :> a" not
R3631 State <> Valid def
R3645 Session <> step_s proj
R3617 Datatypes <> all ind
R3660 Datatypes "l :> a" not
R3631 State <> Valid def
R3645 Session <> step_s proj
R3683 SessionInvariants <> psinv_valid thm
R3683 SessionInvariants <> psinv_valid thm
R3723 State <> Valid def
R3737 Session <> step_s proj
R3723 State <> Valid def
R3737 Session <> step_s proj
R3873 StepInvariants <> inv_valid thm
R3873 StepInvariants <> inv_valid thm
prf 3970 <> psinv_sid
R4055 Datatypes <> all ind
R4086 Coq.Init.Logic "'exists' x : t , p" not
R4157 Coq.Init.Logic "A /\ B" not
R4145 Coq.Init.Logic "x = y" not
R4120 State <> st_session proj
R4132 Session <> step_s proj
R4147 Datatypes <> SomeT constr
R4181 Coq.Init.Logic "x = y" not
R4163 State <> session_suite proj
R4097 State <> SessionInfo rec
R4012 Session <> PartialSession ind
R3996 Datatypes <> seq ind
R4000 Session <> Step rec
R4398 Datatypes <> all_snoc constr
R4398 Datatypes <> all_snoc constr
R4419 Datatypes <> all_nil constr
R4419 Datatypes <> all_nil constr
R4581 Datatypes <> all_snoc constr
R4581 Datatypes <> all_snoc constr
R5275 StepInvariants <> inv_request_session_suite thm
R5275 StepInvariants <> inv_request_session_suite thm
R6698 StepInvariants <> inv_authorization_session_suite thm
R6698 StepInvariants <> inv_authorization_session_suite thm
prf 6889 <> extend_invariant
R7062 Datatypes <> all ind
R6990 Session <> PartialSession ind
R7031 Datatypes "l +> m" not
R7023 Datatypes "l :> a" not
R6968 SessionInvariants <> IsInvariant def
R6956 Session <> Step rec
R6941 Datatypes <> seq ind
R6945 Session <> Step rec
R6941 Datatypes <> seq ind
R6945 Session <> Step rec
R6922 Session <> Step rec
R7217 Datatypes <> all_nil constr
R7217 Datatypes <> all_nil constr
R7355 Datatypes <> all_snoc constr
R7355 Datatypes <> all_snoc constr
R8160 Datatypes <> all ind
R8171 Datatypes "l :> a" not
R8160 Datatypes <> all ind
R8171 Datatypes "l :> a" not
prf 8577 <> session_revoked_is_inv
R8623 SessionInvariants <> IsInvariant def
R8653 Coq.Init.Logic "'exists' x : t , p" not
R8717 Coq.Init.Logic "A /\ B" not
R8705 Coq.Init.Logic "x = y" not
R8683 State <> st_session proj
R8695 Session <> step_s proj
R8707 Datatypes <> SomeT constr
R8720 State <> session_revoked proj
R8664 State <> SessionInfo rec
R8645 Session <> Step rec
R8605 Prelude <> Permission defax
R9661 StepInvariants <> inv_request_allow_blanket_session thm
R9661 StepInvariants <> inv_request_allow_blanket_session thm
R10503 StepInvariants <> inv_request_allow_oneshot_state thm
R10503 StepInvariants <> inv_request_allow_oneshot_state thm
R10878 StepInvariants <> inv_request_deny_blanket_session thm
R10878 StepInvariants <> inv_request_deny_blanket_session thm
R11329 Prelude <> perm_eq_dec prfax
R11329 Prelude <> perm_eq_dec prfax
R11869 StepInvariants <> inv_request_deny_oneshot_state thm
R11869 StepInvariants <> inv_request_deny_oneshot_state thm
R12098 StepInvariants <> inv_request_none_state thm
R12098 StepInvariants <> inv_request_none_state thm
R13872 StepInvariants <> inv_authorization_existent_state thm
R13872 StepInvariants <> inv_authorization_existent_state thm
prf 14388 <> psinv_session_revoked
R14629 Datatypes <> all ind
R14648 Coq.Init.Logic "'exists' x : t , p" not
R14713 Coq.Init.Logic "A /\ B" not
R14701 Coq.Init.Logic "x = y" not
R14679 State <> st_session proj
R14691 Session <> step_s proj
R14703 Datatypes <> SomeT constr
R14716 State <> session_revoked proj
R14659 State <> SessionInfo rec
R14640 Session <> Step rec
R14528 Coq.Init.Logic "'exists' x : t , p" not
R14596 Coq.Init.Logic "A /\ B" not
R14584 Coq.Init.Logic "x = y" not
R14559 State <> st_session proj
R14571 Session <> step_s proj
R14586 Datatypes <> SomeT constr
R14599 State <> session_revoked proj
R14539 State <> SessionInfo rec
R14471 Session <> PartialSession ind
R14512 Datatypes "l +> m" not
R14504 Datatypes "l :> a" not
R14460 Session <> Step rec
R14445 Datatypes <> seq ind
R14449 Session <> Step rec
R14445 Datatypes <> seq ind
R14449 Session <> Step rec
R14426 Prelude <> Permission defax
R14770 SessionInvariants <> extend_invariant thm
R14801 SessionInvariants <> session_revoked_is_inv thm
R14770 SessionInvariants <> extend_invariant thm
R14801 SessionInvariants <> session_revoked_is_inv thm
prf 14983 <> revoke_session_response
R15265 Datatypes <> all ind
R15367 Coq.Init.Logic "x <> y" not
R15355 Session <> step_r proj
R15370 Coq.Init.Datatypes <> Some constr
R15375 Behavior <> allowed constr
R15338 Coq.Init.Logic "x = y" not
R15326 Session <> step_e proj
R15340 Events <> request constr
R15296 Coq.Init.Datatypes <> option ind
R15303 Events <> UserAnswer ind
R15279 Session <> Step rec
R15221 Coq.Init.Logic "x = y" not
R15208 Session <> step_e proj
R15223 Events <> request constr
R15234 Coq.Init.Datatypes <> Some constr
R15240 Events <> ua_deny constr
R15248 Prelude <> session constr
R15139 Behavior <> Pre def
R15165 Events <> request constr
R15176 Coq.Init.Datatypes <> Some constr
R15182 Events <> ua_deny constr
R15190 Prelude <> session constr
R15151 Session <> step_s proj
R15074 Session <> PartialSession ind
R15124 Datatypes "l +> m" not
R15115 Datatypes "l :> a" not
R15107 Datatypes "l :> a" not
R15063 Session <> Step rec
R15063 Session <> Step rec
R15042 Datatypes <> seq ind
R15046 Session <> Step rec
R15042 Datatypes <> seq ind
R15046 Session <> Step rec
R15023 Prelude <> Permission defax
R15610 Datatypes <> all ind
R15647 Coq.Init.Logic "'exists' x : t , p" not
R15705 Coq.Init.Logic "A /\ B" not
R15693 Coq.Init.Logic "x = y" not
R15671 State <> st_session proj
R15683 Session <> step_s proj
R15695 Datatypes <> SomeT constr
R15712 State <> session_revoked proj
R15658 State <> SessionInfo rec
R15621 Session <> Step rec
R15610 Datatypes <> all ind
R15647 Coq.Init.Logic "'exists' x : t , p" not
R15705 Coq.Init.Logic "A /\ B" not
R15693 Coq.Init.Logic "x = y" not
R15671 State <> st_session proj
R15683 Session <> step_s proj
R15695 Datatypes <> SomeT constr
R15712 State <> session_revoked proj
R15658 State <> SessionInfo rec
R15621 Session <> Step rec
R15752 SessionInvariants <> psinv_session_revoked thm
R15752 SessionInvariants <> psinv_session_revoked thm
R16394 Datatypes <> all_nil constr
R16394 Datatypes <> all_nil constr
R16517 Datatypes <> all_snoc constr
R16517 Datatypes <> all_snoc constr
R16540 Datatypes <> all_nil constr
R16540 Datatypes <> all_nil constr
R16857 Coq.Init.Logic "'exists' x : t , p" not
R16921 Coq.Init.Logic "A /\ B" not
R16909 Coq.Init.Logic "x = y" not
R16883 State <> st_session proj
R16895 Session <> step_s proj
R16911 Datatypes <> SomeT constr
R16924 State <> session_revoked proj
R16868 State <> SessionInfo rec
R16857 Coq.Init.Logic "'exists' x : t , p" not
R16921 Coq.Init.Logic "A /\ B" not
R16909 Coq.Init.Logic "x = y" not
R16883 State <> st_session proj
R16895 Session <> step_s proj
R16911 Datatypes <> SomeT constr
R16924 State <> session_revoked proj
R16868 State <> SessionInfo rec
R17542 Datatypes <> all ind
R17595 Datatypes "l :> a" not
R17587 Datatypes "l :> a" not
R17556 State <> Valid def
R17570 Session <> step_s proj
R17542 Datatypes <> all ind
R17595 Datatypes "l :> a" not
R17587 Datatypes "l :> a" not
R17556 State <> Valid def
R17570 Session <> step_s proj
R17620 SessionInvariants <> psinv_valid thm
R17620 SessionInvariants <> psinv_valid thm
R17661 State <> Valid def
R17675 Session <> step_s proj
R17661 State <> Valid def
R17675 Session <> step_s proj
R17831 StepInvariants <> inv_request_revoked_response thm
R17831 StepInvariants <> inv_request_revoked_response thm
R17970 Datatypes <> all_snoc constr
R17970 Datatypes <> all_snoc constr
R18745 Datatypes <> all ind
R18814 Datatypes "l :> a" not
R18807 Datatypes "l +> m" not
R18798 Datatypes "l :> a" not
R18790 Datatypes "l :> a" not
R18759 State <> Valid def
R18773 Session <> step_s proj
R18745 Datatypes <> all ind
R18814 Datatypes "l :> a" not
R18807 Datatypes "l +> m" not
R18798 Datatypes "l :> a" not
R18790 Datatypes "l :> a" not
R18759 State <> Valid def
R18773 Session <> step_s proj
R18835 SessionInvariants <> psinv_valid thm
R18835 SessionInvariants <> psinv_valid thm
R18876 State <> Valid def
R18890 Session <> step_s proj
R18876 State <> Valid def
R18890 Session <> step_s proj
R19086 StepInvariants <> inv_request_revoked_response thm
R19086 StepInvariants <> inv_request_revoked_response thm
prf 19220 <> psinv_valid'
R19239 SessionInvariants <> IsInvariant def
R19266 State <> Valid def
R19280 Session <> step_s proj
R19258 Session <> Step rec
R19348 StepInvariants <> inv_valid thm
R19348 StepInvariants <> inv_valid thm
R19378 SessionInvariants SESSION_INVARIANTS.SOME_INVARIANTS <> sec
sec 19405 SESSION_INVARIANTS AUTHORIZATION_INVARIANTS
var 19441 SESSION_INVARIANTS.AUTHORIZATION_INVARIANTS s0
R19446 State <> State rec
var 19463 SESSION_INVARIANTS.AUTHORIZATION_INVARIANTS sid
R19469 Prelude <> SuiteID defax
var 19664 SESSION_INVARIANTS.AUTHORIZATION_INVARIANTS vr
R19669 Prelude <> VendorRepository rec
var 19697 SESSION_INVARIANTS.AUTHORIZATION_INVARIANTS cert
R19704 Prelude <> Certificate rec
var 19730 SESSION_INVARIANTS.AUTHORIZATION_INVARIANTS HValid
R19739 State <> Valid def
prf 19904 <> psinv_session_unauthorized
R20102 Datatypes <> all ind
R20134 State <> st_unauthorized proj
R20151 Session <> step_s proj
R20113 Session <> Step rec
R20054 State <> st_unauthorized proj
R20071 Session <> step_s proj
R19997 Session <> PartialSession ind
R20039 Datatypes "l +> m" not
R20031 Datatypes "l :> a" not
R19985 Session <> Step rec
R19969 Datatypes <> seq ind
R19973 Session <> Step rec
R19969 Datatypes <> seq ind
R19973 Session <> Step rec
R19952 Prelude <> SuiteID defax
R20369 Datatypes <> all_nil constr
R20369 Datatypes <> all_nil constr
R20420 Datatypes <> all_snoc constr
R20420 Datatypes <> all_snoc constr
R24262 Datatypes <> all ind
R24306 Datatypes "l :> a" not
R24276 State <> Valid def
R24290 Session <> step_s proj
R24262 Datatypes <> all ind
R24306 Datatypes "l :> a" not
R24276 State <> Valid def
R24290 Session <> step_s proj
R24337 SessionInvariants <> psinv_valid thm
R24376 Datatypes "l :> a" not
R24337 SessionInvariants <> psinv_valid thm
R24376 Datatypes "l :> a" not
R24417 State <> Valid def
R24431 Session <> step_s proj
R24417 State <> Valid def
R24431 Session <> step_s proj
R24580 Datatypes <> all ind
R24687 Datatypes "l :> a" not
R24595 Coq.Init.Logic "'exists' x : t , p" not
R24655 Coq.Init.Logic "A /\ B" not
R24643 Coq.Init.Logic "x = y" not
R24620 State <> st_session proj
R24632 Session <> step_s proj
R24645 Datatypes <> SomeT constr
R24676 Coq.Init.Logic "x = y" not
R24658 State <> session_suite proj
R24607 State <> SessionInfo rec
R24580 Datatypes <> all ind
R24687 Datatypes "l :> a" not
R24595 Coq.Init.Logic "'exists' x : t , p" not
R24655 Coq.Init.Logic "A /\ B" not
R24643 Coq.Init.Logic "x = y" not
R24620 State <> st_session proj
R24632 Session <> step_s proj
R24645 Datatypes <> SomeT constr
R24676 Coq.Init.Logic "x = y" not
R24658 State <> session_suite proj
R24607 State <> SessionInfo rec
R24717 SessionInvariants <> psinv_sid thm
R24746 Datatypes "l :> a" not
R24717 SessionInvariants <> psinv_sid thm
R24746 Datatypes "l :> a" not
R24795 Coq.Init.Logic "'exists' x : t , p" not
R24857 Coq.Init.Logic "A /\ B" not
R24845 Coq.Init.Logic "x = y" not
R24820 State <> st_session proj
R24832 Session <> step_s proj
R24847 Datatypes <> SomeT constr
R24878 Coq.Init.Logic "x = y" not
R24860 State <> session_suite proj
R24807 State <> SessionInfo rec
R24795 Coq.Init.Logic "'exists' x : t , p" not
R24857 Coq.Init.Logic "A /\ B" not
R24845 Coq.Init.Logic "x = y" not
R24820 State <> st_session proj
R24832 Session <> step_s proj
R24847 Datatypes <> SomeT constr
R24878 Coq.Init.Logic "x = y" not
R24860 State <> session_suite proj
R24807 State <> SessionInfo rec
R25160 StepInvariants <> inv_install_unauthorized thm
R25193 Session <> step_s proj
R25160 StepInvariants <> inv_install_unauthorized thm
R25193 Session <> step_s proj
R25923 StepInvariants <> inv_authorization_existent_state thm
R25958 Session <> step_s proj
R25923 StepInvariants <> inv_authorization_existent_state thm
R25958 Session <> step_s proj
R26429 Prelude <> sid_eq_dec prfax
R26429 Prelude <> sid_eq_dec prfax
R26721 Datatypes <> all ind
R26886 Datatypes "l :> a" not
R26736 Coq.Init.Logic "'exists' x : t , p" not
R26825 Coq.Init.Logic "A /\ B" not
R26813 Coq.Init.Logic "x = y" not
R26790 State <> st_session proj
R26802 Session <> step_s proj
R26815 Datatypes <> SomeT constr
R26846 Coq.Init.Logic "x = y" not
R26828 State <> session_suite proj
R26748 State <> SessionInfo rec
R26721 Datatypes <> all ind
R26886 Datatypes "l :> a" not
R26736 Coq.Init.Logic "'exists' x : t , p" not
R26825 Coq.Init.Logic "A /\ B" not
R26813 Coq.Init.Logic "x = y" not
R26790 State <> st_session proj
R26802 Session <> step_s proj
R26815 Datatypes <> SomeT constr
R26846 Coq.Init.Logic "x = y" not
R26828 State <> session_suite proj
R26748 State <> SessionInfo rec
R26919 SessionInvariants <> psinv_sid thm
R26948 Datatypes "l :> a" not
R26919 SessionInvariants <> psinv_sid thm
R26948 Datatypes "l :> a" not
R26998 Coq.Init.Logic "'exists' x : t , p" not
R27089 Coq.Init.Logic "A /\ B" not
R27077 Coq.Init.Logic "x = y" not
R27052 State <> st_session proj
R27064 Session <> step_s proj
R27079 Datatypes <> SomeT constr
R27110 Coq.Init.Logic "x = y" not
R27092 State <> session_suite proj
R27010 State <> SessionInfo rec
R26998 Coq.Init.Logic "'exists' x : t , p" not
R27089 Coq.Init.Logic "A /\ B" not
R27077 Coq.Init.Logic "x = y" not
R27052 State <> st_session proj
R27064 Session <> step_s proj
R27079 Datatypes <> SomeT constr
R27110 Coq.Init.Logic "x = y" not
R27092 State <> session_suite proj
R27010 State <> SessionInfo rec
R27677 Datatypes <> all ind
R27813 Datatypes "l :> a" not
R27692 Coq.Init.Logic "'exists' x : t , p" not
R27781 Coq.Init.Logic "A /\ B" not
R27769 Coq.Init.Logic "x = y" not
R27746 State <> st_session proj
R27758 Session <> step_s proj
R27771 Datatypes <> SomeT constr
R27802 Coq.Init.Logic "x = y" not
R27784 State <> session_suite proj
R27704 State <> SessionInfo rec
R27677 Datatypes <> all ind
R27813 Datatypes "l :> a" not
R27692 Coq.Init.Logic "'exists' x : t , p" not
R27781 Coq.Init.Logic "A /\ B" not
R27769 Coq.Init.Logic "x = y" not
R27746 State <> st_session proj
R27758 Session <> step_s proj
R27771 Datatypes <> SomeT constr
R27802 Coq.Init.Logic "x = y" not
R27784 State <> session_suite proj
R27704 State <> SessionInfo rec
R27846 SessionInvariants <> psinv_sid thm
R27875 Datatypes "l :> a" not
R27846 SessionInvariants <> psinv_sid thm
R27875 Datatypes "l :> a" not
R27925 Coq.Init.Logic "'exists' x : t , p" not
R28016 Coq.Init.Logic "A /\ B" not
R28004 Coq.Init.Logic "x = y" not
R27979 State <> st_session proj
R27991 Session <> step_s proj
R28006 Datatypes <> SomeT constr
R28037 Coq.Init.Logic "x = y" not
R28019 State <> session_suite proj
R27937 State <> SessionInfo rec
R27925 Coq.Init.Logic "'exists' x : t , p" not
R28016 Coq.Init.Logic "A /\ B" not
R28004 Coq.Init.Logic "x = y" not
R27979 State <> st_session proj
R27991 Session <> step_s proj
R28006 Datatypes <> SomeT constr
R28037 Coq.Init.Logic "x = y" not
R28019 State <> session_suite proj
R27937 State <> SessionInfo rec
R28568 Datatypes <> all ind
R28632 Datatypes "l :> a" not
R28589 State <> st_unauthorized proj
R28606 Session <> step_s proj
R28581 Session <> Step rec
R28568 Datatypes <> all ind
R28632 Datatypes "l :> a" not
R28589 State <> st_unauthorized proj
R28606 Session <> step_s proj
R28581 Session <> Step rec
R28847 State <> st_unauthorized proj
R28864 Session <> step_s proj
R28847 State <> st_unauthorized proj
R28864 Session <> step_s proj
R32518 Datatypes <> all ind
R32569 Datatypes "l +> m" not
R32562 Datatypes "l :> a" not
R32576 Datatypes "l :> a" not
R32532 State <> Valid def
R32546 Session <> step_s proj
R32518 Datatypes <> all ind
R32569 Datatypes "l +> m" not
R32562 Datatypes "l :> a" not
R32576 Datatypes "l :> a" not
R32532 State <> Valid def
R32546 Session <> step_s proj
R32607 SessionInvariants <> psinv_valid thm
R32652 Datatypes "l +> m" not
R32646 Datatypes "l :> a" not
R32659 Datatypes "l :> a" not
R32607 SessionInvariants <> psinv_valid thm
R32652 Datatypes "l +> m" not
R32646 Datatypes "l :> a" not
R32659 Datatypes "l :> a" not
R32713 State <> Valid def
R32727 Session <> step_s proj
R32713 State <> Valid def
R32727 Session <> step_s proj
R32875 Datatypes <> all ind
R33072 Datatypes "l +> m" not
R33066 Datatypes "l :> a" not
R33079 Datatypes "l :> a" not
R32890 Coq.Init.Logic "'exists' x : t , p" not
R32992 Coq.Init.Logic "A /\ B" not
R32980 Coq.Init.Logic "x = y" not
R32957 State <> st_session proj
R32969 Session <> step_s proj
R32982 Datatypes <> SomeT constr
R33013 Coq.Init.Logic "x = y" not
R32995 State <> session_suite proj
R32902 State <> SessionInfo rec
R32875 Datatypes <> all ind
R33072 Datatypes "l +> m" not
R33066 Datatypes "l :> a" not
R33079 Datatypes "l :> a" not
R32890 Coq.Init.Logic "'exists' x : t , p" not
R32992 Coq.Init.Logic "A /\ B" not
R32980 Coq.Init.Logic "x = y" not
R32957 State <> st_session proj
R32969 Session <> step_s proj
R32982 Datatypes <> SomeT constr
R33013 Coq.Init.Logic "x = y" not
R32995 State <> session_suite proj
R32902 State <> SessionInfo rec
R33110 SessionInvariants <> psinv_sid thm
R33145 Datatypes "l +> m" not
R33139 Datatypes "l :> a" not
R33152 Datatypes "l :> a" not
R33110 SessionInvariants <> psinv_sid thm
R33145 Datatypes "l +> m" not
R33139 Datatypes "l :> a" not
R33152 Datatypes "l :> a" not
R33204 Coq.Init.Logic "'exists' x : t , p" not
R33298 Coq.Init.Logic "A /\ B" not
R33286 Coq.Init.Logic "x = y" not
R33261 State <> st_session proj
R33273 Session <> step_s proj
R33288 Datatypes <> SomeT constr
R33319 Coq.Init.Logic "x = y" not
R33301 State <> session_suite proj
R33216 State <> SessionInfo rec
R33204 Coq.Init.Logic "'exists' x : t , p" not
R33298 Coq.Init.Logic "A /\ B" not
R33286 Coq.Init.Logic "x = y" not
R33261 State <> st_session proj
R33273 Session <> step_s proj
R33288 Datatypes <> SomeT constr
R33319 Coq.Init.Logic "x = y" not
R33301 State <> session_suite proj
R33216 State <> SessionInfo rec
R33658 StepInvariants <> inv_install_unauthorized thm
R33691 Session <> step_s proj
R33658 StepInvariants <> inv_install_unauthorized thm
R33691 Session <> step_s proj
R34445 StepInvariants <> inv_authorization_existent_state thm
R34480 Session <> step_s proj
R34445 StepInvariants <> inv_authorization_existent_state thm
R34480 Session <> step_s proj
R34952 Prelude <> sid_eq_dec prfax
R34952 Prelude <> sid_eq_dec prfax
R35228 Datatypes <> all ind
R35402 Datatypes "l +> m" not
R35396 Datatypes "l :> a" not
R35409 Datatypes "l :> a" not
R35243 Coq.Init.Logic "'exists' x : t , p" not
R35334 Coq.Init.Logic "A /\ B" not
R35322 Coq.Init.Logic "x = y" not
R35299 State <> st_session proj
R35311 Session <> step_s proj
R35324 Datatypes <> SomeT constr
R35355 Coq.Init.Logic "x = y" not
R35337 State <> session_suite proj
R35255 State <> SessionInfo rec
R35228 Datatypes <> all ind
R35402 Datatypes "l +> m" not
R35396 Datatypes "l :> a" not
R35409 Datatypes "l :> a" not
R35243 Coq.Init.Logic "'exists' x : t , p" not
R35334 Coq.Init.Logic "A /\ B" not
R35322 Coq.Init.Logic "x = y" not
R35299 State <> st_session proj
R35311 Session <> step_s proj
R35324 Datatypes <> SomeT constr
R35355 Coq.Init.Logic "x = y" not
R35337 State <> session_suite proj
R35255 State <> SessionInfo rec
R35445 SessionInvariants <> psinv_sid thm
R35480 Datatypes "l +> m" not
R35474 Datatypes "l :> a" not
R35487 Datatypes "l :> a" not
R35445 SessionInvariants <> psinv_sid thm
R35480 Datatypes "l +> m" not
R35474 Datatypes "l :> a" not
R35487 Datatypes "l :> a" not
R35543 Coq.Init.Logic "'exists' x : t , p" not
R35629 Coq.Init.Logic "A /\ B" not
R35617 Coq.Init.Logic "x = y" not
R35592 State <> st_session proj
R35604 Session <> step_s proj
R35619 Datatypes <> SomeT constr
R35650 Coq.Init.Logic "x = y" not
R35632 State <> session_suite proj
R35555 State <> SessionInfo rec
R35543 Coq.Init.Logic "'exists' x : t , p" not
R35629 Coq.Init.Logic "A /\ B" not
R35617 Coq.Init.Logic "x = y" not
R35592 State <> st_session proj
R35604 Session <> step_s proj
R35619 Datatypes <> SomeT constr
R35650 Coq.Init.Logic "x = y" not
R35632 State <> session_suite proj
R35555 State <> SessionInfo rec
R36164 Datatypes <> all ind
R36336 Datatypes "l +> m" not
R36330 Datatypes "l :> a" not
R36343 Datatypes "l :> a" not
R36179 Coq.Init.Logic "'exists' x : t , p" not
R36268 Coq.Init.Logic "A /\ B" not
R36256 Coq.Init.Logic "x = y" not
R36233 State <> st_session proj
R36245 Session <> step_s proj
R36258 Datatypes <> SomeT constr
R36289 Coq.Init.Logic "x = y" not
R36271 State <> session_suite proj
R36191 State <> SessionInfo rec
R36164 Datatypes <> all ind
R36336 Datatypes "l +> m" not
R36330 Datatypes "l :> a" not
R36343 Datatypes "l :> a" not
R36179 Coq.Init.Logic "'exists' x : t , p" not
R36268 Coq.Init.Logic "A /\ B" not
R36256 Coq.Init.Logic "x = y" not
R36233 State <> st_session proj
R36245 Session <> step_s proj
R36258 Datatypes <> SomeT constr
R36289 Coq.Init.Logic "x = y" not
R36271 State <> session_suite proj
R36191 State <> SessionInfo rec
R36379 SessionInvariants <> psinv_sid thm
R36414 Datatypes "l +> m" not
R36408 Datatypes "l :> a" not
R36421 Datatypes "l :> a" not
R36379 SessionInvariants <> psinv_sid thm
R36414 Datatypes "l +> m" not
R36408 Datatypes "l :> a" not
R36421 Datatypes "l :> a" not
R36478 Coq.Init.Logic "'exists' x : t , p" not
R36558 Coq.Init.Logic "A /\ B" not
R36546 Coq.Init.Logic "x = y" not
R36521 State <> st_session proj
R36533 Session <> step_s proj
R36548 Datatypes <> SomeT constr
R36579 Coq.Init.Logic "x = y" not
R36561 State <> session_suite proj
R36490 State <> SessionInfo rec
R36478 Coq.Init.Logic "'exists' x : t , p" not
R36558 Coq.Init.Logic "A /\ B" not
R36546 Coq.Init.Logic "x = y" not
R36521 State <> st_session proj
R36533 Session <> step_s proj
R36548 Datatypes <> SomeT constr
R36579 Coq.Init.Logic "x = y" not
R36561 State <> session_suite proj
R36490 State <> SessionInfo rec
prf 37116 <> unauthorized_response
R37349 Datatypes <> all ind
R37430 Coq.Init.Logic "x <> y" not
R37418 Session <> step_r proj
R37433 Coq.Init.Datatypes <> Some constr
R37438 Behavior <> allowed constr
R37392 Coq.Init.Logic "x = y" not
R37380 Session <> step_e proj
R37394 Events <> authorization constr
R37363 Session <> Step rec
R37312 Coq.Init.Logic "A /\ B" not
R37287 Coq.Init.Logic "x = y" not
R37274 Session <> step_e proj
R37290 Events <> authorization constr
R37328 Coq.Init.Logic "x = y" not
R37315 Session <> step_r proj
R37330 Coq.Init.Datatypes <> Some constr
R37335 Behavior <> denied constr
R37208 Session <> PartialSession ind
R37259 Datatypes "l +> m" not
R37250 Datatypes "l :> a" not
R37242 Datatypes "l :> a" not
R37197 Session <> Step rec
R37197 Session <> Step rec
R37176 Datatypes <> seq ind
R37180 Session <> Step rec
R37176 Datatypes <> seq ind
R37180 Session <> Step rec
R37159 Prelude <> SuiteID defax
R37710 Datatypes <> all ind
R37729 State <> st_unauthorized proj
R37746 Session <> step_s proj
R37721 Session <> Step rec
R37710 Datatypes <> all ind
R37729 State <> st_unauthorized proj
R37746 Session <> step_s proj
R37721 Session <> Step rec
R37784 SessionInvariants <> psinv_session_unauthorized thm
R37784 SessionInvariants <> psinv_session_unauthorized thm
R38231 Datatypes <> all ind
R38413 Datatypes "l :> a" not
R38246 Coq.Init.Logic "'exists' x : t , p" not
R38344 Coq.Init.Logic "A /\ B" not
R38332 Coq.Init.Logic "x = y" not
R38309 State <> st_session proj
R38321 Session <> step_s proj
R38334 Datatypes <> SomeT constr
R38365 Coq.Init.Logic "x = y" not
R38347 State <> session_suite proj
R38258 State <> SessionInfo rec
R38231 Datatypes <> all ind
R38413 Datatypes "l :> a" not
R38246 Coq.Init.Logic "'exists' x : t , p" not
R38344 Coq.Init.Logic "A /\ B" not
R38332 Coq.Init.Logic "x = y" not
R38309 State <> st_session proj
R38321 Session <> step_s proj
R38334 Datatypes <> SomeT constr
R38365 Coq.Init.Logic "x = y" not
R38347 State <> session_suite proj
R38258 State <> SessionInfo rec
R38438 SessionInvariants <> psinv_sid thm
R38438 SessionInvariants <> psinv_sid thm
R38546 Coq.Init.Logic "'exists' x : t , p" not
R38631 Coq.Init.Logic "A /\ B" not
R38619 Coq.Init.Logic "x = y" not
R38594 State <> st_session proj
R38606 Session <> step_s proj
R38621 Datatypes <> SomeT constr
R38652 Coq.Init.Logic "x = y" not
R38634 State <> session_suite proj
R38558 State <> SessionInfo rec
R38546 Coq.Init.Logic "'exists' x : t , p" not
R38631 Coq.Init.Logic "A /\ B" not
R38619 Coq.Init.Logic "x = y" not
R38594 State <> st_session proj
R38606 Session <> step_s proj
R38621 Datatypes <> SomeT constr
R38652 Coq.Init.Logic "x = y" not
R38634 State <> session_suite proj
R38558 State <> SessionInfo rec
R40187 Datatypes <> all_nil constr
R40187 Datatypes <> all_nil constr
R40343 Datatypes <> all_snoc constr
R40343 Datatypes <> all_snoc constr
R40364 Datatypes <> all_nil constr
R40364 Datatypes <> all_nil constr
R40642 Datatypes <> all ind
R40694 Datatypes "l :> a" not
R40686 Datatypes "l :> a" not
R40656 State <> Valid def
R40670 Session <> step_s proj
R40642 Datatypes <> all ind
R40694 Datatypes "l :> a" not
R40686 Datatypes "l :> a" not
R40656 State <> Valid def
R40670 Session <> step_s proj
R40718 SessionInvariants <> psinv_valid thm
R40718 SessionInvariants <> psinv_valid thm
R40830 State <> Valid def
R40844 Session <> step_s proj
R40830 State <> Valid def
R40844 Session <> step_s proj
R40987 Datatypes <> all ind
R41176 Datatypes "l :> a" not
R41170 Datatypes "l :> a" not
R41002 Coq.Init.Logic "'exists' x : t , p" not
R41100 Coq.Init.Logic "A /\ B" not
R41088 Coq.Init.Logic "x = y" not
R41065 State <> st_session proj
R41077 Session <> step_s proj
R41090 Datatypes <> SomeT constr
R41121 Coq.Init.Logic "x = y" not
R41103 State <> session_suite proj
R41014 State <> SessionInfo rec
R40987 Datatypes <> all ind
R41176 Datatypes "l :> a" not
R41170 Datatypes "l :> a" not
R41002 Coq.Init.Logic "'exists' x : t , p" not
R41100 Coq.Init.Logic "A /\ B" not
R41088 Coq.Init.Logic "x = y" not
R41065 State <> st_session proj
R41077 Session <> step_s proj
R41090 Datatypes <> SomeT constr
R41121 Coq.Init.Logic "x = y" not
R41103 State <> session_suite proj
R41014 State <> SessionInfo rec
R41200 SessionInvariants <> psinv_sid thm
R41200 SessionInvariants <> psinv_sid thm
R41294 Coq.Init.Logic "'exists' x : t , p" not
R41391 Coq.Init.Logic "A /\ B" not
R41379 Coq.Init.Logic "x = y" not
R41353 State <> st_session proj
R41365 Session <> step_s proj
R41381 Datatypes <> SomeT constr
R41412 Coq.Init.Logic "x = y" not
R41394 State <> session_suite proj
R41306 State <> SessionInfo rec
R41294 Coq.Init.Logic "'exists' x : t , p" not
R41391 Coq.Init.Logic "A /\ B" not
R41379 Coq.Init.Logic "x = y" not
R41353 State <> st_session proj
R41365 Session <> step_s proj
R41381 Datatypes <> SomeT constr
R41412 Coq.Init.Logic "x = y" not
R41394 State <> session_suite proj
R41306 State <> SessionInfo rec
R41592 State <> st_unauthorized proj
R41609 Session <> step_s proj
R41592 State <> st_unauthorized proj
R41609 Session <> step_s proj
R41800 Datatypes <> all ind
R41983 Datatypes "l :> a" not
R41815 Coq.Init.Logic "'exists' x : t , p" not
R41914 Coq.Init.Logic "A /\ B" not
R41902 Coq.Init.Logic "x = y" not
R41879 State <> st_session proj
R41891 Session <> step_s proj
R41904 Datatypes <> SomeT constr
R41935 Coq.Init.Logic "x = y" not
R41917 State <> session_suite proj
R41827 State <> SessionInfo rec
R41800 Datatypes <> all ind
R41983 Datatypes "l :> a" not
R41815 Coq.Init.Logic "'exists' x : t , p" not
R41914 Coq.Init.Logic "A /\ B" not
R41902 Coq.Init.Logic "x = y" not
R41879 State <> st_session proj
R41891 Session <> step_s proj
R41904 Datatypes <> SomeT constr
R41935 Coq.Init.Logic "x = y" not
R41917 State <> session_suite proj
R41827 State <> SessionInfo rec
R42008 SessionInvariants <> psinv_sid thm
R42008 SessionInvariants <> psinv_sid thm
R42109 Coq.Init.Logic "'exists' x : t , p" not
R42207 Coq.Init.Logic "A /\ B" not
R42195 Coq.Init.Logic "x = y" not
R42170 State <> st_session proj
R42182 Session <> step_s proj
R42197 Datatypes <> SomeT constr
R42228 Coq.Init.Logic "x = y" not
R42210 State <> session_suite proj
R42121 State <> SessionInfo rec
R42109 Coq.Init.Logic "'exists' x : t , p" not
R42207 Coq.Init.Logic "A /\ B" not
R42195 Coq.Init.Logic "x = y" not
R42170 State <> st_session proj
R42182 Session <> step_s proj
R42197 Datatypes <> SomeT constr
R42228 Coq.Init.Logic "x = y" not
R42210 State <> session_suite proj
R42121 State <> SessionInfo rec
R43764 StepInvariants <> inv_authorization_existent_denied_response thm
R43764 StepInvariants <> inv_authorization_existent_denied_response thm
R44088 StepInvariants <> inv_authorization_denied_response thm
R44088 StepInvariants <> inv_authorization_denied_response thm
R44264 Datatypes <> all_snoc constr
R44264 Datatypes <> all_snoc constr
R44735 Datatypes <> all ind
R44938 Datatypes "l :> a" not
R44933 Datatypes "l +> m" not
R44926 Datatypes "l :> a" not
R44920 Datatypes "l :> a" not
R44750 Coq.Init.Logic "'exists' x : t , p" not
R44849 Coq.Init.Logic "A /\ B" not
R44837 Coq.Init.Logic "x = y" not
R44814 State <> st_session proj
R44826 Session <> step_s proj
R44839 Datatypes <> SomeT constr
R44870 Coq.Init.Logic "x = y" not
R44852 State <> session_suite proj
R44762 State <> SessionInfo rec
R44735 Datatypes <> all ind
R44938 Datatypes "l :> a" not
R44933 Datatypes "l +> m" not
R44926 Datatypes "l :> a" not
R44920 Datatypes "l :> a" not
R44750 Coq.Init.Logic "'exists' x : t , p" not
R44849 Coq.Init.Logic "A /\ B" not
R44837 Coq.Init.Logic "x = y" not
R44814 State <> st_session proj
R44826 Session <> step_s proj
R44839 Datatypes <> SomeT constr
R44870 Coq.Init.Logic "x = y" not
R44852 State <> session_suite proj
R44762 State <> SessionInfo rec
R44960 SessionInvariants <> psinv_sid thm
R44960 SessionInvariants <> psinv_sid thm
R45061 Coq.Init.Logic "'exists' x : t , p" not
R45159 Coq.Init.Logic "A /\ B" not
R45147 Coq.Init.Logic "x = y" not
R45125 State <> st_session proj
R45137 Session <> step_s proj
R45149 Datatypes <> SomeT constr
R45180 Coq.Init.Logic "x = y" not
R45162 State <> session_suite proj
R45073 State <> SessionInfo rec
R45061 Coq.Init.Logic "'exists' x : t , p" not
R45159 Coq.Init.Logic "A /\ B" not
R45147 Coq.Init.Logic "x = y" not
R45125 State <> st_session proj
R45137 Session <> step_s proj
R45149 Datatypes <> SomeT constr
R45180 Coq.Init.Logic "x = y" not
R45162 State <> session_suite proj
R45073 State <> SessionInfo rec
R45376 Datatypes <> all ind
R45441 Datatypes "l :> a" not
R45436 Datatypes "l +> m" not
R45428 Datatypes "l :> a" not
R45420 Datatypes "l :> a" not
R45390 State <> Valid def
R45404 Session <> step_s proj
R45376 Datatypes <> all ind
R45441 Datatypes "l :> a" not
R45436 Datatypes "l +> m" not
R45428 Datatypes "l :> a" not
R45420 Datatypes "l :> a" not
R45390 State <> Valid def
R45404 Session <> step_s proj
R45462 SessionInvariants <> psinv_valid thm
R45462 SessionInvariants <> psinv_valid thm
R45578 State <> Valid def
R45592 Session <> step_s proj
R45578 State <> Valid def
R45592 Session <> step_s proj
R46169 StepInvariants <> inv_authorization_existent_denied_response thm
R46169 StepInvariants <> inv_authorization_existent_denied_response thm
R46504 StepInvariants <> inv_authorization_denied_response thm
R46504 StepInvariants <> inv_authorization_denied_response thm
R46601 SessionInvariants SESSION_INVARIANTS.AUTHORIZATION_INVARIANTS <> sec
R46632 SessionInvariants SESSION_INVARIANTS <> sec
